declare INDCONST ac ε NUMBER;

declare INDVAR t1 t2 t3 ε NUMBER;

declare PREDCONST equiv(STATE,STATE,NUMBER);

declare PREDCONST equiva(STATE,STATE,NUMBER);

axiom equiv:
	∀ t eta.equiv(eta,eta,t),
	∀ t eta1 eta2.(equiv(eta1,eta2,t) ⊃ equiv(eta2,eta1,t)),
	∀ t eta1 eta2.(equiva(eta1,eta2,t) ⊃ equiva(eta2,eta1,t)),
	∀ t eta1 eta2 eta3.(equiv(eta1,eta2,t) ∧ equiv(eta2,eta3,t) ⊃
		equiv(eta1,eta3,t)),
	∀ eta1 eta2 t.(equiv(eta1,eta2,t) ⊃ equiva(eta1,eta2,t)),
	∀ t1 t2 eta1 eta2.(t1<t2 ∧ equiv(eta1,eta2,t1) ⊃ equiv(eta1,eta2,t2)),
	∀ t1 t2 eta1 eta2.(t1<t2 ∧ equiva(eta1,eta2,t1) ⊃ equiva(eta1,eta2,t2)),
	∀ t1 t2 n eta.equiv(a(t2,n,eta),eta,t1),
	∀ n eta.equiva(a(ac,n,eta),eta,t),
	∀ t n eta1 eta2.(equiva(eta1,eta2,t) ⊃ equiv(a(ac,n,eta1),a(ac,n,eta2),t)),
	∀ t n eta1 eta2.(equiv(eta1,eta2,t) ⊃ equiv(a(t,n,eta1),a(t,n,eta2),n+1)),
	∀ t n eta1 eta2.(equiva(eta1,eta2,t) ⊃ equiva(a(t,n,eta1),a(t,n,eta2),n+1))
;;